WORST_CASE(?,O(n^3)) * Step 1: DependencyPairs WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: append(dd(x,xs),ys) -> dd(x,append(xs,ys)) append(nil(),ys) -> ys gt(0(),0()) -> false() gt(0(),s(y)) -> false() gt(s(x),0()) -> true() gt(s(x),s(y)) -> gt(x,y) quicksort(dd(z,zs)) -> quicksort'(z,split(z,zs)) quicksort(nil()) -> nil() quicksort'(z,pair(xs,ys)) -> append(quicksort(xs),dd(z,quicksort(ys))) split(pivot,dd(x,xs)) -> split'(gt(x,pivot),x,split(pivot,xs)) split(pivot,nil()) -> pair(nil(),nil()) split'(false(),x,pair(ls,rs)) -> pair(dd(x,ls),rs) split'(true(),x,pair(ls,rs)) -> pair(ls,dd(x,rs)) - Signature: {append/2,gt/2,quicksort/1,quicksort'/2,split/2,split'/3} / {0/0,dd/2,false/0,nil/0,pair/2,s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {append,gt,quicksort,quicksort',split ,split'} and constructors {0,dd,false,nil,pair,s,true} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs append#(dd(x,xs),ys) -> c_1(append#(xs,ys)) append#(nil(),ys) -> c_2() gt#(0(),0()) -> c_3() gt#(0(),s(y)) -> c_4() gt#(s(x),0()) -> c_5() gt#(s(x),s(y)) -> c_6(gt#(x,y)) quicksort#(dd(z,zs)) -> c_7(quicksort'#(z,split(z,zs)),split#(z,zs)) quicksort#(nil()) -> c_8() quicksort'#(z,pair(xs,ys)) -> c_9(append#(quicksort(xs),dd(z,quicksort(ys))),quicksort#(xs),quicksort#(ys)) split#(pivot,dd(x,xs)) -> c_10(split'#(gt(x,pivot),x,split(pivot,xs)),gt#(x,pivot),split#(pivot,xs)) split#(pivot,nil()) -> c_11() split'#(false(),x,pair(ls,rs)) -> c_12() split'#(true(),x,pair(ls,rs)) -> c_13() Weak DPs and mark the set of starting terms. * Step 2: PredecessorEstimation WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: append#(dd(x,xs),ys) -> c_1(append#(xs,ys)) append#(nil(),ys) -> c_2() gt#(0(),0()) -> c_3() gt#(0(),s(y)) -> c_4() gt#(s(x),0()) -> c_5() gt#(s(x),s(y)) -> c_6(gt#(x,y)) quicksort#(dd(z,zs)) -> c_7(quicksort'#(z,split(z,zs)),split#(z,zs)) quicksort#(nil()) -> c_8() quicksort'#(z,pair(xs,ys)) -> c_9(append#(quicksort(xs),dd(z,quicksort(ys))),quicksort#(xs),quicksort#(ys)) split#(pivot,dd(x,xs)) -> c_10(split'#(gt(x,pivot),x,split(pivot,xs)),gt#(x,pivot),split#(pivot,xs)) split#(pivot,nil()) -> c_11() split'#(false(),x,pair(ls,rs)) -> c_12() split'#(true(),x,pair(ls,rs)) -> c_13() - Weak TRS: append(dd(x,xs),ys) -> dd(x,append(xs,ys)) append(nil(),ys) -> ys gt(0(),0()) -> false() gt(0(),s(y)) -> false() gt(s(x),0()) -> true() gt(s(x),s(y)) -> gt(x,y) quicksort(dd(z,zs)) -> quicksort'(z,split(z,zs)) quicksort(nil()) -> nil() quicksort'(z,pair(xs,ys)) -> append(quicksort(xs),dd(z,quicksort(ys))) split(pivot,dd(x,xs)) -> split'(gt(x,pivot),x,split(pivot,xs)) split(pivot,nil()) -> pair(nil(),nil()) split'(false(),x,pair(ls,rs)) -> pair(dd(x,ls),rs) split'(true(),x,pair(ls,rs)) -> pair(ls,dd(x,rs)) - Signature: {append/2,gt/2,quicksort/1,quicksort'/2,split/2,split'/3,append#/2,gt#/2,quicksort#/1,quicksort'#/2,split#/2 ,split'#/3} / {0/0,dd/2,false/0,nil/0,pair/2,s/1,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/2,c_8/0 ,c_9/3,c_10/3,c_11/0,c_12/0,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {append#,gt#,quicksort#,quicksort'#,split# ,split'#} and constructors {0,dd,false,nil,pair,s,true} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {2,3,4,5,8,11,12,13} by application of Pre({2,3,4,5,8,11,12,13}) = {1,6,7,9,10}. Here rules are labelled as follows: 1: append#(dd(x,xs),ys) -> c_1(append#(xs,ys)) 2: append#(nil(),ys) -> c_2() 3: gt#(0(),0()) -> c_3() 4: gt#(0(),s(y)) -> c_4() 5: gt#(s(x),0()) -> c_5() 6: gt#(s(x),s(y)) -> c_6(gt#(x,y)) 7: quicksort#(dd(z,zs)) -> c_7(quicksort'#(z,split(z,zs)),split#(z,zs)) 8: quicksort#(nil()) -> c_8() 9: quicksort'#(z,pair(xs,ys)) -> c_9(append#(quicksort(xs),dd(z,quicksort(ys))) ,quicksort#(xs) ,quicksort#(ys)) 10: split#(pivot,dd(x,xs)) -> c_10(split'#(gt(x,pivot),x,split(pivot,xs)),gt#(x,pivot),split#(pivot,xs)) 11: split#(pivot,nil()) -> c_11() 12: split'#(false(),x,pair(ls,rs)) -> c_12() 13: split'#(true(),x,pair(ls,rs)) -> c_13() * Step 3: RemoveWeakSuffixes WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: append#(dd(x,xs),ys) -> c_1(append#(xs,ys)) gt#(s(x),s(y)) -> c_6(gt#(x,y)) quicksort#(dd(z,zs)) -> c_7(quicksort'#(z,split(z,zs)),split#(z,zs)) quicksort'#(z,pair(xs,ys)) -> c_9(append#(quicksort(xs),dd(z,quicksort(ys))),quicksort#(xs),quicksort#(ys)) split#(pivot,dd(x,xs)) -> c_10(split'#(gt(x,pivot),x,split(pivot,xs)),gt#(x,pivot),split#(pivot,xs)) - Weak DPs: append#(nil(),ys) -> c_2() gt#(0(),0()) -> c_3() gt#(0(),s(y)) -> c_4() gt#(s(x),0()) -> c_5() quicksort#(nil()) -> c_8() split#(pivot,nil()) -> c_11() split'#(false(),x,pair(ls,rs)) -> c_12() split'#(true(),x,pair(ls,rs)) -> c_13() - Weak TRS: append(dd(x,xs),ys) -> dd(x,append(xs,ys)) append(nil(),ys) -> ys gt(0(),0()) -> false() gt(0(),s(y)) -> false() gt(s(x),0()) -> true() gt(s(x),s(y)) -> gt(x,y) quicksort(dd(z,zs)) -> quicksort'(z,split(z,zs)) quicksort(nil()) -> nil() quicksort'(z,pair(xs,ys)) -> append(quicksort(xs),dd(z,quicksort(ys))) split(pivot,dd(x,xs)) -> split'(gt(x,pivot),x,split(pivot,xs)) split(pivot,nil()) -> pair(nil(),nil()) split'(false(),x,pair(ls,rs)) -> pair(dd(x,ls),rs) split'(true(),x,pair(ls,rs)) -> pair(ls,dd(x,rs)) - Signature: {append/2,gt/2,quicksort/1,quicksort'/2,split/2,split'/3,append#/2,gt#/2,quicksort#/1,quicksort'#/2,split#/2 ,split'#/3} / {0/0,dd/2,false/0,nil/0,pair/2,s/1,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/2,c_8/0 ,c_9/3,c_10/3,c_11/0,c_12/0,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {append#,gt#,quicksort#,quicksort'#,split# ,split'#} and constructors {0,dd,false,nil,pair,s,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:append#(dd(x,xs),ys) -> c_1(append#(xs,ys)) -->_1 append#(nil(),ys) -> c_2():6 -->_1 append#(dd(x,xs),ys) -> c_1(append#(xs,ys)):1 2:S:gt#(s(x),s(y)) -> c_6(gt#(x,y)) -->_1 gt#(s(x),0()) -> c_5():9 -->_1 gt#(0(),s(y)) -> c_4():8 -->_1 gt#(0(),0()) -> c_3():7 -->_1 gt#(s(x),s(y)) -> c_6(gt#(x,y)):2 3:S:quicksort#(dd(z,zs)) -> c_7(quicksort'#(z,split(z,zs)),split#(z,zs)) -->_2 split#(pivot,dd(x,xs)) -> c_10(split'#(gt(x,pivot),x,split(pivot,xs)) ,gt#(x,pivot) ,split#(pivot,xs)):5 -->_1 quicksort'#(z,pair(xs,ys)) -> c_9(append#(quicksort(xs),dd(z,quicksort(ys))) ,quicksort#(xs) ,quicksort#(ys)):4 -->_2 split#(pivot,nil()) -> c_11():11 4:S:quicksort'#(z,pair(xs,ys)) -> c_9(append#(quicksort(xs),dd(z,quicksort(ys))) ,quicksort#(xs) ,quicksort#(ys)) -->_3 quicksort#(nil()) -> c_8():10 -->_2 quicksort#(nil()) -> c_8():10 -->_1 append#(nil(),ys) -> c_2():6 -->_3 quicksort#(dd(z,zs)) -> c_7(quicksort'#(z,split(z,zs)),split#(z,zs)):3 -->_2 quicksort#(dd(z,zs)) -> c_7(quicksort'#(z,split(z,zs)),split#(z,zs)):3 -->_1 append#(dd(x,xs),ys) -> c_1(append#(xs,ys)):1 5:S:split#(pivot,dd(x,xs)) -> c_10(split'#(gt(x,pivot),x,split(pivot,xs)),gt#(x,pivot),split#(pivot,xs)) -->_1 split'#(true(),x,pair(ls,rs)) -> c_13():13 -->_1 split'#(false(),x,pair(ls,rs)) -> c_12():12 -->_3 split#(pivot,nil()) -> c_11():11 -->_2 gt#(s(x),0()) -> c_5():9 -->_2 gt#(0(),s(y)) -> c_4():8 -->_2 gt#(0(),0()) -> c_3():7 -->_3 split#(pivot,dd(x,xs)) -> c_10(split'#(gt(x,pivot),x,split(pivot,xs)) ,gt#(x,pivot) ,split#(pivot,xs)):5 -->_2 gt#(s(x),s(y)) -> c_6(gt#(x,y)):2 6:W:append#(nil(),ys) -> c_2() 7:W:gt#(0(),0()) -> c_3() 8:W:gt#(0(),s(y)) -> c_4() 9:W:gt#(s(x),0()) -> c_5() 10:W:quicksort#(nil()) -> c_8() 11:W:split#(pivot,nil()) -> c_11() 12:W:split'#(false(),x,pair(ls,rs)) -> c_12() 13:W:split'#(true(),x,pair(ls,rs)) -> c_13() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 10: quicksort#(nil()) -> c_8() 11: split#(pivot,nil()) -> c_11() 12: split'#(false(),x,pair(ls,rs)) -> c_12() 13: split'#(true(),x,pair(ls,rs)) -> c_13() 7: gt#(0(),0()) -> c_3() 8: gt#(0(),s(y)) -> c_4() 9: gt#(s(x),0()) -> c_5() 6: append#(nil(),ys) -> c_2() * Step 4: SimplifyRHS WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: append#(dd(x,xs),ys) -> c_1(append#(xs,ys)) gt#(s(x),s(y)) -> c_6(gt#(x,y)) quicksort#(dd(z,zs)) -> c_7(quicksort'#(z,split(z,zs)),split#(z,zs)) quicksort'#(z,pair(xs,ys)) -> c_9(append#(quicksort(xs),dd(z,quicksort(ys))),quicksort#(xs),quicksort#(ys)) split#(pivot,dd(x,xs)) -> c_10(split'#(gt(x,pivot),x,split(pivot,xs)),gt#(x,pivot),split#(pivot,xs)) - Weak TRS: append(dd(x,xs),ys) -> dd(x,append(xs,ys)) append(nil(),ys) -> ys gt(0(),0()) -> false() gt(0(),s(y)) -> false() gt(s(x),0()) -> true() gt(s(x),s(y)) -> gt(x,y) quicksort(dd(z,zs)) -> quicksort'(z,split(z,zs)) quicksort(nil()) -> nil() quicksort'(z,pair(xs,ys)) -> append(quicksort(xs),dd(z,quicksort(ys))) split(pivot,dd(x,xs)) -> split'(gt(x,pivot),x,split(pivot,xs)) split(pivot,nil()) -> pair(nil(),nil()) split'(false(),x,pair(ls,rs)) -> pair(dd(x,ls),rs) split'(true(),x,pair(ls,rs)) -> pair(ls,dd(x,rs)) - Signature: {append/2,gt/2,quicksort/1,quicksort'/2,split/2,split'/3,append#/2,gt#/2,quicksort#/1,quicksort'#/2,split#/2 ,split'#/3} / {0/0,dd/2,false/0,nil/0,pair/2,s/1,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/2,c_8/0 ,c_9/3,c_10/3,c_11/0,c_12/0,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {append#,gt#,quicksort#,quicksort'#,split# ,split'#} and constructors {0,dd,false,nil,pair,s,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:append#(dd(x,xs),ys) -> c_1(append#(xs,ys)) -->_1 append#(dd(x,xs),ys) -> c_1(append#(xs,ys)):1 2:S:gt#(s(x),s(y)) -> c_6(gt#(x,y)) -->_1 gt#(s(x),s(y)) -> c_6(gt#(x,y)):2 3:S:quicksort#(dd(z,zs)) -> c_7(quicksort'#(z,split(z,zs)),split#(z,zs)) -->_2 split#(pivot,dd(x,xs)) -> c_10(split'#(gt(x,pivot),x,split(pivot,xs)) ,gt#(x,pivot) ,split#(pivot,xs)):5 -->_1 quicksort'#(z,pair(xs,ys)) -> c_9(append#(quicksort(xs),dd(z,quicksort(ys))) ,quicksort#(xs) ,quicksort#(ys)):4 4:S:quicksort'#(z,pair(xs,ys)) -> c_9(append#(quicksort(xs),dd(z,quicksort(ys))) ,quicksort#(xs) ,quicksort#(ys)) -->_3 quicksort#(dd(z,zs)) -> c_7(quicksort'#(z,split(z,zs)),split#(z,zs)):3 -->_2 quicksort#(dd(z,zs)) -> c_7(quicksort'#(z,split(z,zs)),split#(z,zs)):3 -->_1 append#(dd(x,xs),ys) -> c_1(append#(xs,ys)):1 5:S:split#(pivot,dd(x,xs)) -> c_10(split'#(gt(x,pivot),x,split(pivot,xs)),gt#(x,pivot),split#(pivot,xs)) -->_3 split#(pivot,dd(x,xs)) -> c_10(split'#(gt(x,pivot),x,split(pivot,xs)) ,gt#(x,pivot) ,split#(pivot,xs)):5 -->_2 gt#(s(x),s(y)) -> c_6(gt#(x,y)):2 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: split#(pivot,dd(x,xs)) -> c_10(gt#(x,pivot),split#(pivot,xs)) * Step 5: DecomposeDG WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: append#(dd(x,xs),ys) -> c_1(append#(xs,ys)) gt#(s(x),s(y)) -> c_6(gt#(x,y)) quicksort#(dd(z,zs)) -> c_7(quicksort'#(z,split(z,zs)),split#(z,zs)) quicksort'#(z,pair(xs,ys)) -> c_9(append#(quicksort(xs),dd(z,quicksort(ys))),quicksort#(xs),quicksort#(ys)) split#(pivot,dd(x,xs)) -> c_10(gt#(x,pivot),split#(pivot,xs)) - Weak TRS: append(dd(x,xs),ys) -> dd(x,append(xs,ys)) append(nil(),ys) -> ys gt(0(),0()) -> false() gt(0(),s(y)) -> false() gt(s(x),0()) -> true() gt(s(x),s(y)) -> gt(x,y) quicksort(dd(z,zs)) -> quicksort'(z,split(z,zs)) quicksort(nil()) -> nil() quicksort'(z,pair(xs,ys)) -> append(quicksort(xs),dd(z,quicksort(ys))) split(pivot,dd(x,xs)) -> split'(gt(x,pivot),x,split(pivot,xs)) split(pivot,nil()) -> pair(nil(),nil()) split'(false(),x,pair(ls,rs)) -> pair(dd(x,ls),rs) split'(true(),x,pair(ls,rs)) -> pair(ls,dd(x,rs)) - Signature: {append/2,gt/2,quicksort/1,quicksort'/2,split/2,split'/3,append#/2,gt#/2,quicksort#/1,quicksort'#/2,split#/2 ,split'#/3} / {0/0,dd/2,false/0,nil/0,pair/2,s/1,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/2,c_8/0 ,c_9/3,c_10/2,c_11/0,c_12/0,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {append#,gt#,quicksort#,quicksort'#,split# ,split'#} and constructors {0,dd,false,nil,pair,s,true} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component quicksort#(dd(z,zs)) -> c_7(quicksort'#(z,split(z,zs)),split#(z,zs)) quicksort'#(z,pair(xs,ys)) -> c_9(append#(quicksort(xs),dd(z,quicksort(ys))),quicksort#(xs),quicksort#(ys)) and a lower component append#(dd(x,xs),ys) -> c_1(append#(xs,ys)) gt#(s(x),s(y)) -> c_6(gt#(x,y)) split#(pivot,dd(x,xs)) -> c_10(gt#(x,pivot),split#(pivot,xs)) Further, following extension rules are added to the lower component. quicksort#(dd(z,zs)) -> quicksort'#(z,split(z,zs)) quicksort#(dd(z,zs)) -> split#(z,zs) quicksort'#(z,pair(xs,ys)) -> append#(quicksort(xs),dd(z,quicksort(ys))) quicksort'#(z,pair(xs,ys)) -> quicksort#(xs) quicksort'#(z,pair(xs,ys)) -> quicksort#(ys) ** Step 5.a:1: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: quicksort#(dd(z,zs)) -> c_7(quicksort'#(z,split(z,zs)),split#(z,zs)) quicksort'#(z,pair(xs,ys)) -> c_9(append#(quicksort(xs),dd(z,quicksort(ys))),quicksort#(xs),quicksort#(ys)) - Weak TRS: append(dd(x,xs),ys) -> dd(x,append(xs,ys)) append(nil(),ys) -> ys gt(0(),0()) -> false() gt(0(),s(y)) -> false() gt(s(x),0()) -> true() gt(s(x),s(y)) -> gt(x,y) quicksort(dd(z,zs)) -> quicksort'(z,split(z,zs)) quicksort(nil()) -> nil() quicksort'(z,pair(xs,ys)) -> append(quicksort(xs),dd(z,quicksort(ys))) split(pivot,dd(x,xs)) -> split'(gt(x,pivot),x,split(pivot,xs)) split(pivot,nil()) -> pair(nil(),nil()) split'(false(),x,pair(ls,rs)) -> pair(dd(x,ls),rs) split'(true(),x,pair(ls,rs)) -> pair(ls,dd(x,rs)) - Signature: {append/2,gt/2,quicksort/1,quicksort'/2,split/2,split'/3,append#/2,gt#/2,quicksort#/1,quicksort'#/2,split#/2 ,split'#/3} / {0/0,dd/2,false/0,nil/0,pair/2,s/1,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/2,c_8/0 ,c_9/3,c_10/2,c_11/0,c_12/0,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {append#,gt#,quicksort#,quicksort'#,split# ,split'#} and constructors {0,dd,false,nil,pair,s,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:quicksort#(dd(z,zs)) -> c_7(quicksort'#(z,split(z,zs)),split#(z,zs)) -->_1 quicksort'#(z,pair(xs,ys)) -> c_9(append#(quicksort(xs),dd(z,quicksort(ys))) ,quicksort#(xs) ,quicksort#(ys)):2 2:S:quicksort'#(z,pair(xs,ys)) -> c_9(append#(quicksort(xs),dd(z,quicksort(ys))) ,quicksort#(xs) ,quicksort#(ys)) -->_3 quicksort#(dd(z,zs)) -> c_7(quicksort'#(z,split(z,zs)),split#(z,zs)):1 -->_2 quicksort#(dd(z,zs)) -> c_7(quicksort'#(z,split(z,zs)),split#(z,zs)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: quicksort#(dd(z,zs)) -> c_7(quicksort'#(z,split(z,zs))) quicksort'#(z,pair(xs,ys)) -> c_9(quicksort#(xs),quicksort#(ys)) ** Step 5.a:2: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: quicksort#(dd(z,zs)) -> c_7(quicksort'#(z,split(z,zs))) quicksort'#(z,pair(xs,ys)) -> c_9(quicksort#(xs),quicksort#(ys)) - Weak TRS: append(dd(x,xs),ys) -> dd(x,append(xs,ys)) append(nil(),ys) -> ys gt(0(),0()) -> false() gt(0(),s(y)) -> false() gt(s(x),0()) -> true() gt(s(x),s(y)) -> gt(x,y) quicksort(dd(z,zs)) -> quicksort'(z,split(z,zs)) quicksort(nil()) -> nil() quicksort'(z,pair(xs,ys)) -> append(quicksort(xs),dd(z,quicksort(ys))) split(pivot,dd(x,xs)) -> split'(gt(x,pivot),x,split(pivot,xs)) split(pivot,nil()) -> pair(nil(),nil()) split'(false(),x,pair(ls,rs)) -> pair(dd(x,ls),rs) split'(true(),x,pair(ls,rs)) -> pair(ls,dd(x,rs)) - Signature: {append/2,gt/2,quicksort/1,quicksort'/2,split/2,split'/3,append#/2,gt#/2,quicksort#/1,quicksort'#/2,split#/2 ,split'#/3} / {0/0,dd/2,false/0,nil/0,pair/2,s/1,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/1,c_8/0 ,c_9/2,c_10/2,c_11/0,c_12/0,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {append#,gt#,quicksort#,quicksort'#,split# ,split'#} and constructors {0,dd,false,nil,pair,s,true} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: gt(0(),0()) -> false() gt(0(),s(y)) -> false() gt(s(x),0()) -> true() gt(s(x),s(y)) -> gt(x,y) split(pivot,dd(x,xs)) -> split'(gt(x,pivot),x,split(pivot,xs)) split(pivot,nil()) -> pair(nil(),nil()) split'(false(),x,pair(ls,rs)) -> pair(dd(x,ls),rs) split'(true(),x,pair(ls,rs)) -> pair(ls,dd(x,rs)) quicksort#(dd(z,zs)) -> c_7(quicksort'#(z,split(z,zs))) quicksort'#(z,pair(xs,ys)) -> c_9(quicksort#(xs),quicksort#(ys)) ** Step 5.a:3: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: quicksort#(dd(z,zs)) -> c_7(quicksort'#(z,split(z,zs))) quicksort'#(z,pair(xs,ys)) -> c_9(quicksort#(xs),quicksort#(ys)) - Weak TRS: gt(0(),0()) -> false() gt(0(),s(y)) -> false() gt(s(x),0()) -> true() gt(s(x),s(y)) -> gt(x,y) split(pivot,dd(x,xs)) -> split'(gt(x,pivot),x,split(pivot,xs)) split(pivot,nil()) -> pair(nil(),nil()) split'(false(),x,pair(ls,rs)) -> pair(dd(x,ls),rs) split'(true(),x,pair(ls,rs)) -> pair(ls,dd(x,rs)) - Signature: {append/2,gt/2,quicksort/1,quicksort'/2,split/2,split'/3,append#/2,gt#/2,quicksort#/1,quicksort'#/2,split#/2 ,split'#/3} / {0/0,dd/2,false/0,nil/0,pair/2,s/1,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/1,c_8/0 ,c_9/2,c_10/2,c_11/0,c_12/0,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {append#,gt#,quicksort#,quicksort'#,split# ,split'#} and constructors {0,dd,false,nil,pair,s,true} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- 0 :: [] -(0)-> "A"(0) dd :: ["A"(0) x "A"(2)] -(2)-> "A"(2) false :: [] -(0)-> "A"(0) false :: [] -(0)-> "A"(15) gt :: ["A"(0) x "A"(0)] -(0)-> "A"(9) nil :: [] -(0)-> "A"(2) nil :: [] -(0)-> "A"(15) pair :: ["A"(2) x "A"(2)] -(0)-> "A"(2) pair :: ["A"(15) x "A"(15)] -(0)-> "A"(15) s :: ["A"(0)] -(0)-> "A"(0) split :: ["A"(0) x "A"(2)] -(0)-> "A"(2) split' :: ["A"(0) x "A"(0) x "A"(2)] -(2)-> "A"(2) true :: [] -(0)-> "A"(0) true :: [] -(0)-> "A"(15) quicksort# :: ["A"(2)] -(0)-> "A"(4) quicksort'# :: ["A"(0) x "A"(2)] -(1)-> "A"(13) c_7 :: ["A"(0)] -(0)-> "A"(12) c_9 :: ["A"(0) x "A"(0)] -(0)-> "A"(15) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "0_A" :: [] -(0)-> "A"(1) "c_7_A" :: ["A"(0)] -(0)-> "A"(1) "c_9_A" :: ["A"(0) x "A"(0)] -(0)-> "A"(1) "dd_A" :: ["A"(0) x "A"(1)] -(1)-> "A"(1) "false_A" :: [] -(0)-> "A"(1) "nil_A" :: [] -(0)-> "A"(1) "pair_A" :: ["A"(1) x "A"(1)] -(0)-> "A"(1) "s_A" :: ["A"(1)] -(1)-> "A"(1) "true_A" :: [] -(0)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: quicksort#(dd(z,zs)) -> c_7(quicksort'#(z,split(z,zs))) quicksort'#(z,pair(xs,ys)) -> c_9(quicksort#(xs),quicksort#(ys)) 2. Weak: ** Step 5.b:1: DecomposeDG WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: append#(dd(x,xs),ys) -> c_1(append#(xs,ys)) gt#(s(x),s(y)) -> c_6(gt#(x,y)) split#(pivot,dd(x,xs)) -> c_10(gt#(x,pivot),split#(pivot,xs)) - Weak DPs: quicksort#(dd(z,zs)) -> quicksort'#(z,split(z,zs)) quicksort#(dd(z,zs)) -> split#(z,zs) quicksort'#(z,pair(xs,ys)) -> append#(quicksort(xs),dd(z,quicksort(ys))) quicksort'#(z,pair(xs,ys)) -> quicksort#(xs) quicksort'#(z,pair(xs,ys)) -> quicksort#(ys) - Weak TRS: append(dd(x,xs),ys) -> dd(x,append(xs,ys)) append(nil(),ys) -> ys gt(0(),0()) -> false() gt(0(),s(y)) -> false() gt(s(x),0()) -> true() gt(s(x),s(y)) -> gt(x,y) quicksort(dd(z,zs)) -> quicksort'(z,split(z,zs)) quicksort(nil()) -> nil() quicksort'(z,pair(xs,ys)) -> append(quicksort(xs),dd(z,quicksort(ys))) split(pivot,dd(x,xs)) -> split'(gt(x,pivot),x,split(pivot,xs)) split(pivot,nil()) -> pair(nil(),nil()) split'(false(),x,pair(ls,rs)) -> pair(dd(x,ls),rs) split'(true(),x,pair(ls,rs)) -> pair(ls,dd(x,rs)) - Signature: {append/2,gt/2,quicksort/1,quicksort'/2,split/2,split'/3,append#/2,gt#/2,quicksort#/1,quicksort'#/2,split#/2 ,split'#/3} / {0/0,dd/2,false/0,nil/0,pair/2,s/1,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/2,c_8/0 ,c_9/3,c_10/2,c_11/0,c_12/0,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {append#,gt#,quicksort#,quicksort'#,split# ,split'#} and constructors {0,dd,false,nil,pair,s,true} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component append#(dd(x,xs),ys) -> c_1(append#(xs,ys)) quicksort#(dd(z,zs)) -> quicksort'#(z,split(z,zs)) quicksort#(dd(z,zs)) -> split#(z,zs) quicksort'#(z,pair(xs,ys)) -> append#(quicksort(xs),dd(z,quicksort(ys))) quicksort'#(z,pair(xs,ys)) -> quicksort#(xs) quicksort'#(z,pair(xs,ys)) -> quicksort#(ys) split#(pivot,dd(x,xs)) -> c_10(gt#(x,pivot),split#(pivot,xs)) and a lower component gt#(s(x),s(y)) -> c_6(gt#(x,y)) Further, following extension rules are added to the lower component. append#(dd(x,xs),ys) -> append#(xs,ys) quicksort#(dd(z,zs)) -> quicksort'#(z,split(z,zs)) quicksort#(dd(z,zs)) -> split#(z,zs) quicksort'#(z,pair(xs,ys)) -> append#(quicksort(xs),dd(z,quicksort(ys))) quicksort'#(z,pair(xs,ys)) -> quicksort#(xs) quicksort'#(z,pair(xs,ys)) -> quicksort#(ys) split#(pivot,dd(x,xs)) -> gt#(x,pivot) split#(pivot,dd(x,xs)) -> split#(pivot,xs) *** Step 5.b:1.a:1: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: append#(dd(x,xs),ys) -> c_1(append#(xs,ys)) split#(pivot,dd(x,xs)) -> c_10(gt#(x,pivot),split#(pivot,xs)) - Weak DPs: quicksort#(dd(z,zs)) -> quicksort'#(z,split(z,zs)) quicksort#(dd(z,zs)) -> split#(z,zs) quicksort'#(z,pair(xs,ys)) -> append#(quicksort(xs),dd(z,quicksort(ys))) quicksort'#(z,pair(xs,ys)) -> quicksort#(xs) quicksort'#(z,pair(xs,ys)) -> quicksort#(ys) - Weak TRS: append(dd(x,xs),ys) -> dd(x,append(xs,ys)) append(nil(),ys) -> ys gt(0(),0()) -> false() gt(0(),s(y)) -> false() gt(s(x),0()) -> true() gt(s(x),s(y)) -> gt(x,y) quicksort(dd(z,zs)) -> quicksort'(z,split(z,zs)) quicksort(nil()) -> nil() quicksort'(z,pair(xs,ys)) -> append(quicksort(xs),dd(z,quicksort(ys))) split(pivot,dd(x,xs)) -> split'(gt(x,pivot),x,split(pivot,xs)) split(pivot,nil()) -> pair(nil(),nil()) split'(false(),x,pair(ls,rs)) -> pair(dd(x,ls),rs) split'(true(),x,pair(ls,rs)) -> pair(ls,dd(x,rs)) - Signature: {append/2,gt/2,quicksort/1,quicksort'/2,split/2,split'/3,append#/2,gt#/2,quicksort#/1,quicksort'#/2,split#/2 ,split'#/3} / {0/0,dd/2,false/0,nil/0,pair/2,s/1,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/2,c_8/0 ,c_9/3,c_10/2,c_11/0,c_12/0,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {append#,gt#,quicksort#,quicksort'#,split# ,split'#} and constructors {0,dd,false,nil,pair,s,true} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:append#(dd(x,xs),ys) -> c_1(append#(xs,ys)) -->_1 append#(dd(x,xs),ys) -> c_1(append#(xs,ys)):1 2:S:split#(pivot,dd(x,xs)) -> c_10(gt#(x,pivot),split#(pivot,xs)) -->_2 split#(pivot,dd(x,xs)) -> c_10(gt#(x,pivot),split#(pivot,xs)):2 3:W:quicksort#(dd(z,zs)) -> quicksort'#(z,split(z,zs)) -->_1 quicksort'#(z,pair(xs,ys)) -> quicksort#(ys):7 -->_1 quicksort'#(z,pair(xs,ys)) -> quicksort#(xs):6 -->_1 quicksort'#(z,pair(xs,ys)) -> append#(quicksort(xs),dd(z,quicksort(ys))):5 4:W:quicksort#(dd(z,zs)) -> split#(z,zs) -->_1 split#(pivot,dd(x,xs)) -> c_10(gt#(x,pivot),split#(pivot,xs)):2 5:W:quicksort'#(z,pair(xs,ys)) -> append#(quicksort(xs),dd(z,quicksort(ys))) -->_1 append#(dd(x,xs),ys) -> c_1(append#(xs,ys)):1 6:W:quicksort'#(z,pair(xs,ys)) -> quicksort#(xs) -->_1 quicksort#(dd(z,zs)) -> split#(z,zs):4 -->_1 quicksort#(dd(z,zs)) -> quicksort'#(z,split(z,zs)):3 7:W:quicksort'#(z,pair(xs,ys)) -> quicksort#(ys) -->_1 quicksort#(dd(z,zs)) -> split#(z,zs):4 -->_1 quicksort#(dd(z,zs)) -> quicksort'#(z,split(z,zs)):3 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: split#(pivot,dd(x,xs)) -> c_10(split#(pivot,xs)) *** Step 5.b:1.a:2: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: append#(dd(x,xs),ys) -> c_1(append#(xs,ys)) split#(pivot,dd(x,xs)) -> c_10(split#(pivot,xs)) - Weak DPs: quicksort#(dd(z,zs)) -> quicksort'#(z,split(z,zs)) quicksort#(dd(z,zs)) -> split#(z,zs) quicksort'#(z,pair(xs,ys)) -> append#(quicksort(xs),dd(z,quicksort(ys))) quicksort'#(z,pair(xs,ys)) -> quicksort#(xs) quicksort'#(z,pair(xs,ys)) -> quicksort#(ys) - Weak TRS: append(dd(x,xs),ys) -> dd(x,append(xs,ys)) append(nil(),ys) -> ys gt(0(),0()) -> false() gt(0(),s(y)) -> false() gt(s(x),0()) -> true() gt(s(x),s(y)) -> gt(x,y) quicksort(dd(z,zs)) -> quicksort'(z,split(z,zs)) quicksort(nil()) -> nil() quicksort'(z,pair(xs,ys)) -> append(quicksort(xs),dd(z,quicksort(ys))) split(pivot,dd(x,xs)) -> split'(gt(x,pivot),x,split(pivot,xs)) split(pivot,nil()) -> pair(nil(),nil()) split'(false(),x,pair(ls,rs)) -> pair(dd(x,ls),rs) split'(true(),x,pair(ls,rs)) -> pair(ls,dd(x,rs)) - Signature: {append/2,gt/2,quicksort/1,quicksort'/2,split/2,split'/3,append#/2,gt#/2,quicksort#/1,quicksort'#/2,split#/2 ,split'#/3} / {0/0,dd/2,false/0,nil/0,pair/2,s/1,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/2,c_8/0 ,c_9/3,c_10/1,c_11/0,c_12/0,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {append#,gt#,quicksort#,quicksort'#,split# ,split'#} and constructors {0,dd,false,nil,pair,s,true} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- 0 :: [] -(0)-> "A"(0) append :: ["A"(5) x "A"(5)] -(9)-> "A"(5) dd :: ["A"(0) x "A"(0)] -(0)-> "A"(0) dd :: ["A"(0) x "A"(15)] -(15)-> "A"(15) dd :: ["A"(0) x "A"(5)] -(5)-> "A"(5) dd :: ["A"(0) x "A"(1)] -(1)-> "A"(1) false :: [] -(0)-> "A"(0) false :: [] -(0)-> "A"(15) gt :: ["A"(0) x "A"(0)] -(0)-> "A"(9) nil :: [] -(0)-> "A"(5) nil :: [] -(0)-> "A"(15) nil :: [] -(0)-> "A"(11) pair :: ["A"(15) x "A"(15)] -(0)-> "A"(15) quicksort :: ["A"(15)] -(0)-> "A"(5) quicksort' :: ["A"(0) x "A"(15)] -(15)-> "A"(5) s :: ["A"(0)] -(0)-> "A"(0) split :: ["A"(0) x "A"(15)] -(0)-> "A"(15) split' :: ["A"(0) x "A"(0) x "A"(15)] -(15)-> "A"(15) true :: [] -(0)-> "A"(0) true :: [] -(0)-> "A"(15) append# :: ["A"(0) x "A"(0)] -(0)-> "A"(1) quicksort# :: ["A"(15)] -(2)-> "A"(1) quicksort'# :: ["A"(0) x "A"(15)] -(6)-> "A"(1) split# :: ["A"(0) x "A"(15)] -(8)-> "A"(1) c_1 :: ["A"(0)] -(0)-> "A"(12) c_10 :: ["A"(0)] -(0)-> "A"(12) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "0_A" :: [] -(0)-> "A"(1) "c_10_A" :: ["A"(0)] -(0)-> "A"(1) "c_1_A" :: ["A"(0)] -(0)-> "A"(1) "dd_A" :: ["A"(0) x "A"(1)] -(1)-> "A"(1) "false_A" :: [] -(0)-> "A"(1) "nil_A" :: [] -(0)-> "A"(1) "pair_A" :: ["A"(1) x "A"(1)] -(0)-> "A"(1) "s_A" :: ["A"(0)] -(0)-> "A"(1) "true_A" :: [] -(0)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: split#(pivot,dd(x,xs)) -> c_10(split#(pivot,xs)) 2. Weak: append#(dd(x,xs),ys) -> c_1(append#(xs,ys)) *** Step 5.b:1.a:3: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: append#(dd(x,xs),ys) -> c_1(append#(xs,ys)) - Weak DPs: quicksort#(dd(z,zs)) -> quicksort'#(z,split(z,zs)) quicksort#(dd(z,zs)) -> split#(z,zs) quicksort'#(z,pair(xs,ys)) -> append#(quicksort(xs),dd(z,quicksort(ys))) quicksort'#(z,pair(xs,ys)) -> quicksort#(xs) quicksort'#(z,pair(xs,ys)) -> quicksort#(ys) split#(pivot,dd(x,xs)) -> c_10(split#(pivot,xs)) - Weak TRS: append(dd(x,xs),ys) -> dd(x,append(xs,ys)) append(nil(),ys) -> ys gt(0(),0()) -> false() gt(0(),s(y)) -> false() gt(s(x),0()) -> true() gt(s(x),s(y)) -> gt(x,y) quicksort(dd(z,zs)) -> quicksort'(z,split(z,zs)) quicksort(nil()) -> nil() quicksort'(z,pair(xs,ys)) -> append(quicksort(xs),dd(z,quicksort(ys))) split(pivot,dd(x,xs)) -> split'(gt(x,pivot),x,split(pivot,xs)) split(pivot,nil()) -> pair(nil(),nil()) split'(false(),x,pair(ls,rs)) -> pair(dd(x,ls),rs) split'(true(),x,pair(ls,rs)) -> pair(ls,dd(x,rs)) - Signature: {append/2,gt/2,quicksort/1,quicksort'/2,split/2,split'/3,append#/2,gt#/2,quicksort#/1,quicksort'#/2,split#/2 ,split'#/3} / {0/0,dd/2,false/0,nil/0,pair/2,s/1,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/2,c_8/0 ,c_9/3,c_10/1,c_11/0,c_12/0,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {append#,gt#,quicksort#,quicksort'#,split# ,split'#} and constructors {0,dd,false,nil,pair,s,true} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- 0 :: [] -(0)-> "A"(0) append :: ["A"(1) x "A"(1)] -(0)-> "A"(1) dd :: ["A"(0) x "A"(1)] -(1)-> "A"(1) dd :: ["A"(0) x "A"(8)] -(8)-> "A"(8) dd :: ["A"(0) x "A"(7)] -(7)-> "A"(7) dd :: ["A"(0) x "A"(0)] -(0)-> "A"(0) false :: [] -(0)-> "A"(0) false :: [] -(0)-> "A"(15) gt :: ["A"(0) x "A"(0)] -(0)-> "A"(9) nil :: [] -(0)-> "A"(1) nil :: [] -(0)-> "A"(8) nil :: [] -(0)-> "A"(7) nil :: [] -(0)-> "A"(15) pair :: ["A"(8) x "A"(8)] -(0)-> "A"(8) pair :: ["A"(10) x "A"(10)] -(0)-> "A"(10) quicksort :: ["A"(8)] -(0)-> "A"(1) quicksort' :: ["A"(0) x "A"(8)] -(4)-> "A"(1) s :: ["A"(0)] -(0)-> "A"(0) split :: ["A"(0) x "A"(8)] -(0)-> "A"(8) split' :: ["A"(0) x "A"(0) x "A"(8)] -(8)-> "A"(8) true :: [] -(0)-> "A"(0) true :: [] -(0)-> "A"(15) append# :: ["A"(1) x "A"(0)] -(0)-> "A"(1) quicksort# :: ["A"(8)] -(9)-> "A"(1) quicksort'# :: ["A"(0) x "A"(8)] -(13)-> "A"(1) split# :: ["A"(0) x "A"(7)] -(9)-> "A"(12) c_1 :: ["A"(0)] -(0)-> "A"(12) c_10 :: ["A"(0)] -(0)-> "A"(15) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "0_A" :: [] -(0)-> "A"(1) "c_10_A" :: ["A"(0)] -(0)-> "A"(1) "c_1_A" :: ["A"(0)] -(0)-> "A"(1) "dd_A" :: ["A"(0) x "A"(1)] -(1)-> "A"(1) "false_A" :: [] -(0)-> "A"(1) "nil_A" :: [] -(0)-> "A"(1) "pair_A" :: ["A"(1) x "A"(1)] -(0)-> "A"(1) "s_A" :: ["A"(0)] -(0)-> "A"(1) "true_A" :: [] -(0)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: append#(dd(x,xs),ys) -> c_1(append#(xs,ys)) 2. Weak: *** Step 5.b:1.b:1: RemoveWeakSuffixes WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: gt#(s(x),s(y)) -> c_6(gt#(x,y)) - Weak DPs: append#(dd(x,xs),ys) -> append#(xs,ys) quicksort#(dd(z,zs)) -> quicksort'#(z,split(z,zs)) quicksort#(dd(z,zs)) -> split#(z,zs) quicksort'#(z,pair(xs,ys)) -> append#(quicksort(xs),dd(z,quicksort(ys))) quicksort'#(z,pair(xs,ys)) -> quicksort#(xs) quicksort'#(z,pair(xs,ys)) -> quicksort#(ys) split#(pivot,dd(x,xs)) -> gt#(x,pivot) split#(pivot,dd(x,xs)) -> split#(pivot,xs) - Weak TRS: append(dd(x,xs),ys) -> dd(x,append(xs,ys)) append(nil(),ys) -> ys gt(0(),0()) -> false() gt(0(),s(y)) -> false() gt(s(x),0()) -> true() gt(s(x),s(y)) -> gt(x,y) quicksort(dd(z,zs)) -> quicksort'(z,split(z,zs)) quicksort(nil()) -> nil() quicksort'(z,pair(xs,ys)) -> append(quicksort(xs),dd(z,quicksort(ys))) split(pivot,dd(x,xs)) -> split'(gt(x,pivot),x,split(pivot,xs)) split(pivot,nil()) -> pair(nil(),nil()) split'(false(),x,pair(ls,rs)) -> pair(dd(x,ls),rs) split'(true(),x,pair(ls,rs)) -> pair(ls,dd(x,rs)) - Signature: {append/2,gt/2,quicksort/1,quicksort'/2,split/2,split'/3,append#/2,gt#/2,quicksort#/1,quicksort'#/2,split#/2 ,split'#/3} / {0/0,dd/2,false/0,nil/0,pair/2,s/1,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/2,c_8/0 ,c_9/3,c_10/2,c_11/0,c_12/0,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {append#,gt#,quicksort#,quicksort'#,split# ,split'#} and constructors {0,dd,false,nil,pair,s,true} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:gt#(s(x),s(y)) -> c_6(gt#(x,y)) -->_1 gt#(s(x),s(y)) -> c_6(gt#(x,y)):1 2:W:append#(dd(x,xs),ys) -> append#(xs,ys) -->_1 append#(dd(x,xs),ys) -> append#(xs,ys):2 3:W:quicksort#(dd(z,zs)) -> quicksort'#(z,split(z,zs)) -->_1 quicksort'#(z,pair(xs,ys)) -> quicksort#(ys):7 -->_1 quicksort'#(z,pair(xs,ys)) -> quicksort#(xs):6 -->_1 quicksort'#(z,pair(xs,ys)) -> append#(quicksort(xs),dd(z,quicksort(ys))):5 4:W:quicksort#(dd(z,zs)) -> split#(z,zs) -->_1 split#(pivot,dd(x,xs)) -> split#(pivot,xs):9 -->_1 split#(pivot,dd(x,xs)) -> gt#(x,pivot):8 5:W:quicksort'#(z,pair(xs,ys)) -> append#(quicksort(xs),dd(z,quicksort(ys))) -->_1 append#(dd(x,xs),ys) -> append#(xs,ys):2 6:W:quicksort'#(z,pair(xs,ys)) -> quicksort#(xs) -->_1 quicksort#(dd(z,zs)) -> split#(z,zs):4 -->_1 quicksort#(dd(z,zs)) -> quicksort'#(z,split(z,zs)):3 7:W:quicksort'#(z,pair(xs,ys)) -> quicksort#(ys) -->_1 quicksort#(dd(z,zs)) -> split#(z,zs):4 -->_1 quicksort#(dd(z,zs)) -> quicksort'#(z,split(z,zs)):3 8:W:split#(pivot,dd(x,xs)) -> gt#(x,pivot) -->_1 gt#(s(x),s(y)) -> c_6(gt#(x,y)):1 9:W:split#(pivot,dd(x,xs)) -> split#(pivot,xs) -->_1 split#(pivot,dd(x,xs)) -> split#(pivot,xs):9 -->_1 split#(pivot,dd(x,xs)) -> gt#(x,pivot):8 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 5: quicksort'#(z,pair(xs,ys)) -> append#(quicksort(xs),dd(z,quicksort(ys))) 2: append#(dd(x,xs),ys) -> append#(xs,ys) *** Step 5.b:1.b:2: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: gt#(s(x),s(y)) -> c_6(gt#(x,y)) - Weak DPs: quicksort#(dd(z,zs)) -> quicksort'#(z,split(z,zs)) quicksort#(dd(z,zs)) -> split#(z,zs) quicksort'#(z,pair(xs,ys)) -> quicksort#(xs) quicksort'#(z,pair(xs,ys)) -> quicksort#(ys) split#(pivot,dd(x,xs)) -> gt#(x,pivot) split#(pivot,dd(x,xs)) -> split#(pivot,xs) - Weak TRS: append(dd(x,xs),ys) -> dd(x,append(xs,ys)) append(nil(),ys) -> ys gt(0(),0()) -> false() gt(0(),s(y)) -> false() gt(s(x),0()) -> true() gt(s(x),s(y)) -> gt(x,y) quicksort(dd(z,zs)) -> quicksort'(z,split(z,zs)) quicksort(nil()) -> nil() quicksort'(z,pair(xs,ys)) -> append(quicksort(xs),dd(z,quicksort(ys))) split(pivot,dd(x,xs)) -> split'(gt(x,pivot),x,split(pivot,xs)) split(pivot,nil()) -> pair(nil(),nil()) split'(false(),x,pair(ls,rs)) -> pair(dd(x,ls),rs) split'(true(),x,pair(ls,rs)) -> pair(ls,dd(x,rs)) - Signature: {append/2,gt/2,quicksort/1,quicksort'/2,split/2,split'/3,append#/2,gt#/2,quicksort#/1,quicksort'#/2,split#/2 ,split'#/3} / {0/0,dd/2,false/0,nil/0,pair/2,s/1,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/2,c_8/0 ,c_9/3,c_10/2,c_11/0,c_12/0,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {append#,gt#,quicksort#,quicksort'#,split# ,split'#} and constructors {0,dd,false,nil,pair,s,true} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: gt(0(),0()) -> false() gt(0(),s(y)) -> false() gt(s(x),0()) -> true() gt(s(x),s(y)) -> gt(x,y) split(pivot,dd(x,xs)) -> split'(gt(x,pivot),x,split(pivot,xs)) split(pivot,nil()) -> pair(nil(),nil()) split'(false(),x,pair(ls,rs)) -> pair(dd(x,ls),rs) split'(true(),x,pair(ls,rs)) -> pair(ls,dd(x,rs)) gt#(s(x),s(y)) -> c_6(gt#(x,y)) quicksort#(dd(z,zs)) -> quicksort'#(z,split(z,zs)) quicksort#(dd(z,zs)) -> split#(z,zs) quicksort'#(z,pair(xs,ys)) -> quicksort#(xs) quicksort'#(z,pair(xs,ys)) -> quicksort#(ys) split#(pivot,dd(x,xs)) -> gt#(x,pivot) split#(pivot,dd(x,xs)) -> split#(pivot,xs) *** Step 5.b:1.b:3: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: gt#(s(x),s(y)) -> c_6(gt#(x,y)) - Weak DPs: quicksort#(dd(z,zs)) -> quicksort'#(z,split(z,zs)) quicksort#(dd(z,zs)) -> split#(z,zs) quicksort'#(z,pair(xs,ys)) -> quicksort#(xs) quicksort'#(z,pair(xs,ys)) -> quicksort#(ys) split#(pivot,dd(x,xs)) -> gt#(x,pivot) split#(pivot,dd(x,xs)) -> split#(pivot,xs) - Weak TRS: gt(0(),0()) -> false() gt(0(),s(y)) -> false() gt(s(x),0()) -> true() gt(s(x),s(y)) -> gt(x,y) split(pivot,dd(x,xs)) -> split'(gt(x,pivot),x,split(pivot,xs)) split(pivot,nil()) -> pair(nil(),nil()) split'(false(),x,pair(ls,rs)) -> pair(dd(x,ls),rs) split'(true(),x,pair(ls,rs)) -> pair(ls,dd(x,rs)) - Signature: {append/2,gt/2,quicksort/1,quicksort'/2,split/2,split'/3,append#/2,gt#/2,quicksort#/1,quicksort'#/2,split#/2 ,split'#/3} / {0/0,dd/2,false/0,nil/0,pair/2,s/1,true/0,c_1/1,c_2/0,c_3/0,c_4/0,c_5/0,c_6/1,c_7/2,c_8/0 ,c_9/3,c_10/2,c_11/0,c_12/0,c_13/0} - Obligation: innermost runtime complexity wrt. defined symbols {append#,gt#,quicksort#,quicksort'#,split# ,split'#} and constructors {0,dd,false,nil,pair,s,true} + Applied Processor: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- 0 :: [] -(0)-> "A"(0) dd :: ["A"(6) x "A"(6)] -(6)-> "A"(6) false :: [] -(0)-> "A"(0) false :: [] -(0)-> "A"(14) gt :: ["A"(0) x "A"(0)] -(0)-> "A"(0) nil :: [] -(0)-> "A"(6) nil :: [] -(0)-> "A"(14) pair :: ["A"(6) x "A"(6)] -(0)-> "A"(6) pair :: ["A"(14) x "A"(14)] -(0)-> "A"(14) s :: ["A"(0)] -(0)-> "A"(0) s :: ["A"(1)] -(1)-> "A"(1) split :: ["A"(0) x "A"(6)] -(1)-> "A"(6) split' :: ["A"(0) x "A"(6) x "A"(6)] -(6)-> "A"(6) true :: [] -(0)-> "A"(0) true :: [] -(0)-> "A"(14) gt# :: ["A"(0) x "A"(1)] -(6)-> "A"(0) quicksort# :: ["A"(6)] -(14)-> "A"(0) quicksort'# :: ["A"(0) x "A"(6)] -(15)-> "A"(0) split# :: ["A"(5) x "A"(6)] -(5)-> "A"(0) c_6 :: ["A"(0)] -(0)-> "A"(14) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "0_A" :: [] -(0)-> "A"(1) "c_6_A" :: ["A"(0)] -(0)-> "A"(1) "dd_A" :: ["A"(1) x "A"(1)] -(1)-> "A"(1) "false_A" :: [] -(0)-> "A"(1) "nil_A" :: [] -(0)-> "A"(1) "pair_A" :: ["A"(1) x "A"(1)] -(0)-> "A"(1) "s_A" :: ["A"(1)] -(1)-> "A"(1) "true_A" :: [] -(0)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: gt#(s(x),s(y)) -> c_6(gt#(x,y)) 2. Weak: WORST_CASE(?,O(n^3))